E:Type, T, V:(IdIdType), M:(IdLnkIdType), pred?:(E(E+Unit)),
info:(E(IdId+(IdLnkE)Id)), init:(i,x:IdT(i,x)),
Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x))),
val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) )).
(e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 SWellFounded(pred!(e;e'))
 (e:E. state_when(e)  x:IdT(loc(e),x)) 

latex

Definitions	t  T, Id, x:A. B(x), loc(e), f(a), x:AB(x), x.A(x), x. t(x), 1of(t), x:AB(x), P  Q, when-after(e;info;pred?;init;Trans;val), s = t, state_when(e), Type, IdLnk, Unit, left+right, x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, kind(e), pred(e), Prop, first(e), b, A, pred!(e;e'), SWellFounded(R(x;y))
Lemmas	strongwellfounded wf, pred! wf, not wf, assert wf, first wf, pred wf, kind wf, Knd wf, kindcase wf, unit wf, IdLnk wf, when-after wf, pi1 wf, loc wf, Id wf